Model: | embedded v.1 (CTMC) |
Parameter(s) | MAX_COUNT = 8, T = 12 |
Property: | actuators (prob-reach) |
mcsta/modest mcsta embedded.jani -E MAX_COUNT=8,T=12 --props actuators -O out.txt Minimal --unsafe --es -S Memory --no-partial-results --p0 --p1
Walltime: | 7.284163236618042s |
Return code: | 0 |
Note(s): | The tool result '646935642857007/6250000000000000' is tagged as incorrect. The reference result is '2486339329126654286603009697501669410565922080647235572297420531003436740865701642894224651957236979415804844019970070797212838741320749871087696043790430488516768144231337033817746564261751745074561347394006816495027017797689319547300488225074500148562849173672852142305219348461967484204844049064729196699735928014471258755257981315981437194941990940151801223037104684834501918219518509576147895594521550143080313306069328271572867233516691965651482621705351476665971739605138196440899155147689763504549588268208121401875264463514032072760483012146809591389917819090345027584564812047944749664670576370371539376963526238191240909958985452275278006429583432435031807238331342878089585624527146895090748546393263058273883548791148930403418281798548198424839109773636808627978181634014955673865189747661646872651996258392552936446048778850218123619968642035042613279480618036150872134108049644406926052409061681799637826350380022669199996003596956454782552145333056157894145489486150540020412367389756815095367155100979032989577219964876141639524244527608740339422128257119204903748534580255367130745069830155822896692205418889181867570399342666796568670310583910515081237965368477709014032538181219194690388788147910806457016503932544044361342482618424045300689342156932654513810653232/23611139712102051230917389163705830960031855919193061353466918264830083378326191986369644719731733927229539492600419384037259194731474764121283541927110582338954972260482489069672524784993784262550354865456872177586787640220120819688039079785300002792915291730955593483931646644219725546280035297145057925920216590907280123192615618204899469159482885775117640880607396241557854775904114044868093404127365731780383766098536743365431606149805147123738769862714193052746662633506746823832901275751745965930188386773348462353851130634494111719846304545619011283033383773694078253680336971342463788449790335853827682934039541430969389834393278233712786556823508225268957600063594542555015850051657407051988438160129534133247921531327619001040045086238243881240503946765414870850573700427770606192511529412103367398696559809991483002140786128316014280845971470100880405232693440182197432483126227685144563355464988202359315240457890538240804613319209327258473954661426136227180487183808347011148390279684571713981594509718194717843432940624635810976882203361528885015337153218704100617865345448218447207127579308191723103792137390005496384380796220104269395092237919302086773300230575431863081466614429004067089423894856968938002028941688162575178715549796054402371237245066557533118053584375' (approx. 0.1053036557931282) which means a relative error of '0.01703599863172215' which is larger than the goal precision '0.001'. |
Relative Error: | 0.01703599863172215 |
embedded.jani:model: info: embedded is a CTMC model. embedded.jani: info: Need 16 bytes per state. embedded.jani: info: Explored 5820 states for MAX_COUNT=8, T=12.0. Peak memory usage: 53 MB Analysis results for embedded.jani Experiment MAX_COUNT=8, T=12.0 + State space exploration State size: 16 bytes States: 5820 Transitions: 5820 Branches: 16788 Rate: 85588 states/s Time: 0.1 s + Property actuators Probability: 0.10350970285712112 Bounds: [0.10350970285712112, 1] Time: 6.7 s + Precomputations Min. prob. 0 states: 4512 Time for min. prob. 0 states: 0.0 s Min. prob. 1 states: 180 Time for min. prob. 1 states: 0.0 s + Essential states Iterations: 1 Essential states: 1130 Transitions: 1130 Branches: 7386 Time: 0.0 s + Value iteration Final error: 9.999901531850148E-07 Iterations: 94800 Time: 6.7 s Exported results to file "/out.txt".
The Modest Toolset (www.modestchecker.net), version v3.1.42-gb5e9d523c.